Nuprl Lemma : Rall-nil
11,40
postcript
pdf
R
:top. sqequal(Rall([];
x
.
R
(
x
)); Rnone)
latex
Definitions
t
T
,
reduce(
f
;
k
;
as
)
,
Y
,
map(
f
;
as
)
,
Rlist(
L
)
,
Rall(
L
;
x
.
R
(
x
))
,
x
:
A
.
B
(
x
)
Lemmas
top
wf
origin
R:top. sqequal(Rall([]; x.R(x)); Rnone) R:top. sqequal(Rall([]; x.R(x)); Rnone) 
Tx:A. B(x)